Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_20 (Apple Inc.) Main-Class: Carre

class Curseur{
	private int X=0, Y=0, maxX, maxY;
	private boolean torique=false;

	public Curseur(int maxX, int maxY, boolean espaceTorique){
		super();
		this.maxX=maxX;
		this.maxY=maxY;
		this.torique=espaceTorique;		
	}

	public void centrer(){
		
			int cX=maxX/2;
			int cY=maxY/2;
			X=cX;
			Y=cY;
		
	}

	public void haut(){

			Y--;
			if(torique&&Y<0) Y=maxY-1;
	}

	public void bas(){
			Y++;
			if(torique&&Y==maxY) Y=0;
	}

	public void droite(){
			X++;
			if(torique&&X==maxX) X=0;
	}

	public void gauche(){
			X--;
			if(torique&&X<0) X=maxX-1;
	}

	public int getX(){
			return X;
	}

	public int getY(){
			return Y;
	}
	
	public void imprimer(){
	    //System.out.println("Curseur@["+getX()+","+getY()+"]");
	}
}

public class Carre {

	private Curseur curseur=null;
	private int cote=0;

	public Carre(int cote){
		if(cote>1&cote%2==1){
			this.cote=cote; 
		}else{
		    //System.out.println("Cette classe ne genere pas les carres magiques d\'ordre pair.");
		    //System.exit(0);
		}
		this.curseur=new Curseur(cote,cote,true);
	}
	
	private int [][] carre=null;

	public void init(){
		carre=new int[cote][cote];
		int n=0;
		for(int x=0;x<3;x++) for(int y=0;y<3;y++) carre[x][y]=0;
		curseur.centrer();
	}

	public void peupler(){
		curseur.bas();
		int nbre=1;
		int cpteur=1;
		while(cpteur<3){			
			if(!ajouter(nbre,curseur.getX(),curseur.getY())){
				curseur.bas();
				curseur.gauche();
				cpteur++;
			}else{
				cpteur=1;
				curseur.bas();
				curseur.droite();
				nbre++;
			}
		}
	}

	public Curseur curseur(){
		return curseur;
	}

	public int cote(){
		return cote;
	}

	public boolean ajouter(int nombre, int X, int Y){
		if(carre[X][Y]!=0) return false; 
		carre[X][Y]=nombre;
		return true;
	}

	public void imprimer(){
		for(int j=0;j<cote;j++){
			for(int i=0;i<cote;i++){
			    //System.out.print(carre[i][j]+"\t");
			}
			//System.out.println();
		}
	}

	public static void main(String args[]){
	    Random.args = args;
	    Carre carre=new Carre(2*Random.random()+1);
	    carre.init();
	    //carre.peupler();
	    carre.imprimer();
	}
    
}

public class Random {
  static String[] args;
  static int index = 0;

  public static int random() {
      if (index >= args.length)
	  return 0;

      String string = args[index];
      index++;
      return string.length();
  }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Carre.main([Ljava/lang/String;)V: Graph of 611 nodes with 2 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 2 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Carre.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses: UsedFieldsAnalysis

(6) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 24 rules for P and 0 rules for R.

P rules:
2927_0_imprimer_Load(EOS(STATIC_2927), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i433) → 2929_0_imprimer_FieldAccess(EOS(STATIC_2929), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i433, java.lang.Object(Carre(EOC, i27)))
2929_0_imprimer_FieldAccess(EOS(STATIC_2929), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i433, java.lang.Object(Carre(EOC, i27))) → 2930_0_imprimer_GE(EOS(STATIC_2930), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i433, i27)
2930_0_imprimer_GE(EOS(STATIC_2930), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i433, i27) → 2933_0_imprimer_GE(EOS(STATIC_2933), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i433, i27)
2933_0_imprimer_GE(EOS(STATIC_2933), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i433, i27) → 2936_0_imprimer_ConstantStackPush(EOS(STATIC_2936), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433) | <(i433, i27)
2936_0_imprimer_ConstantStackPush(EOS(STATIC_2936), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433) → 2939_0_imprimer_Store(EOS(STATIC_2939), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, 0)
2939_0_imprimer_Store(EOS(STATIC_2939), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, matching1) → 2942_0_imprimer_Load(EOS(STATIC_2942), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, 0) | =(matching1, 0)
2942_0_imprimer_Load(EOS(STATIC_2942), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, matching1) → 2956_0_imprimer_Load(EOS(STATIC_2956), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, 0) | =(matching1, 0)
2956_0_imprimer_Load(EOS(STATIC_2956), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i435) → 2970_0_imprimer_Load(EOS(STATIC_2970), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i435)
2970_0_imprimer_Load(EOS(STATIC_2970), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i438) → 2993_0_imprimer_Load(EOS(STATIC_2993), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i438)
2993_0_imprimer_Load(EOS(STATIC_2993), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i443) → 3185_0_imprimer_Load(EOS(STATIC_3185), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i443)
3185_0_imprimer_Load(EOS(STATIC_3185), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i636) → 3349_0_imprimer_Load(EOS(STATIC_3349), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i636, i636)
3349_0_imprimer_Load(EOS(STATIC_3349), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i636, i636) → 3351_0_imprimer_FieldAccess(EOS(STATIC_3351), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i636, i636, java.lang.Object(Carre(EOC, i27)))
3351_0_imprimer_FieldAccess(EOS(STATIC_3351), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i636, i636, java.lang.Object(Carre(EOC, i27))) → 3352_0_imprimer_GE(EOS(STATIC_3352), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i636, i636, i27)
3352_0_imprimer_GE(EOS(STATIC_3352), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i636, i636, i27) → 3354_0_imprimer_GE(EOS(STATIC_3354), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i636, i636, i27)
3352_0_imprimer_GE(EOS(STATIC_3352), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i636, i636, i27) → 3355_0_imprimer_GE(EOS(STATIC_3355), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i636, i636, i27)
3354_0_imprimer_GE(EOS(STATIC_3354), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i636, i636, i27) → 3356_0_imprimer_Inc(EOS(STATIC_3356), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433) | >=(i636, i27)
3356_0_imprimer_Inc(EOS(STATIC_3356), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433) → 3359_0_imprimer_JMP(EOS(STATIC_3359), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), +(i433, 1)) | >=(i433, 0)
3359_0_imprimer_JMP(EOS(STATIC_3359), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i825) → 3364_0_imprimer_Load(EOS(STATIC_3364), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i825)
3364_0_imprimer_Load(EOS(STATIC_3364), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i825) → 2925_0_imprimer_Load(EOS(STATIC_2925), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i825)
2925_0_imprimer_Load(EOS(STATIC_2925), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433) → 2927_0_imprimer_Load(EOS(STATIC_2927), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i433)
3355_0_imprimer_GE(EOS(STATIC_3355), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i636, i636, i27) → 3358_0_imprimer_Inc(EOS(STATIC_3358), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i636) | <(i636, i27)
3358_0_imprimer_Inc(EOS(STATIC_3358), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i636) → 3361_0_imprimer_JMP(EOS(STATIC_3361), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, +(i636, 1)) | >=(i636, 0)
3361_0_imprimer_JMP(EOS(STATIC_3361), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i826) → 3367_0_imprimer_Load(EOS(STATIC_3367), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i826)
3367_0_imprimer_Load(EOS(STATIC_3367), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i826) → 3185_0_imprimer_Load(EOS(STATIC_3185), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i433, i826)
R rules:

Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.

P rules:
3352_0_imprimer_GE(EOS(STATIC_3352), java.lang.Object(Carre(EOC, x0)), java.lang.Object(Carre(EOC, x0)), x1, x2, x2, x0) → 3352_0_imprimer_GE(EOS(STATIC_3352), java.lang.Object(Carre(EOC, x0)), java.lang.Object(Carre(EOC, x0)), +(x1, 1), 0, 0, x0) | &&(&&(>=(x2, x0), >(+(x1, 1), 0)), >(x0, +(x1, 1)))
3352_0_imprimer_GE(EOS(STATIC_3352), java.lang.Object(Carre(EOC, x0)), java.lang.Object(Carre(EOC, x0)), x1, x2, x2, x0) → 3352_0_imprimer_GE(EOS(STATIC_3352), java.lang.Object(Carre(EOC, x0)), java.lang.Object(Carre(EOC, x0)), x1, +(x2, 1), +(x2, 1), x0) | &&(>(+(x2, 1), 0), <(x2, x0))
R rules:

Filtered ground terms:

3352_0_imprimer_GE(x1, x2, x3, x4, x5, x6, x7) → 3352_0_imprimer_GE(x2, x3, x4, x5, x6, x7)
Carre(x1, x2) → Carre(x2)
EOS(x1) → EOS
Cond_3352_0_imprimer_GE1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_3352_0_imprimer_GE1(x1, x3, x4, x5, x6, x7, x8)
Cond_3352_0_imprimer_GE(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_3352_0_imprimer_GE(x1, x3, x4, x5, x6, x7, x8)

Filtered duplicate args:

3352_0_imprimer_GE(x1, x2, x3, x4, x5, x6) → 3352_0_imprimer_GE(x2, x3, x5)
Cond_3352_0_imprimer_GE(x1, x2, x3, x4, x5, x6, x7) → Cond_3352_0_imprimer_GE(x1, x3, x4, x6)
Cond_3352_0_imprimer_GE1(x1, x2, x3, x4, x5, x6, x7) → Cond_3352_0_imprimer_GE1(x1, x3, x4, x6)

Filtered unneeded arguments:

Cond_3352_0_imprimer_GE(x1, x2, x3, x4) → Cond_3352_0_imprimer_GE(x1, x2, x3)

Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.

P rules:
3352_0_imprimer_GE(java.lang.Object(Carre(x0)), x1, x2) → 3352_0_imprimer_GE(java.lang.Object(Carre(x0)), +(x1, 1), 0) | &&(&&(>=(x2, x0), >(x1, -1)), >(x0, +(x1, 1)))
3352_0_imprimer_GE(java.lang.Object(Carre(x0)), x1, x2) → 3352_0_imprimer_GE(java.lang.Object(Carre(x0)), x1, +(x2, 1)) | &&(>(x2, -1), <(x2, x0))
R rules:

Finished conversion. Obtained 4 rules for P and 0 rules for R. System has predefined symbols.

P rules:
3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0)), x1, x2) → COND_3352_0_IMPRIMER_GE(&&(&&(>=(x2, x0), >(x1, -1)), >(x0, +(x1, 1))), java.lang.Object(Carre(x0)), x1, x2)
COND_3352_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0)), x1, x2) → 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0)), +(x1, 1), 0)
3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0)), x1, x2) → COND_3352_0_IMPRIMER_GE1(&&(>(x2, -1), <(x2, x0)), java.lang.Object(Carre(x0)), x1, x2)
COND_3352_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0)), x1, x2) → 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0)), x1, +(x2, 1))
R rules:

(7) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
||	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), x1[0], x2[0]) → COND_3352_0_IMPRIMER_GE(x2[0] >= x0[0] && x1[0] > -1 && x0[0] > x1[0] + 1, java.lang.Object(Carre(x0[0])), x1[0], x2[0])
(1): COND_3352_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0[1])), x1[1], x2[1]) → 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), x1[1] + 1, 0)
(2): 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_3352_0_IMPRIMER_GE1(x2[2] > -1 && x2[2] < x0[2], java.lang.Object(Carre(x0[2])), x1[2], x2[2])
(3): COND_3352_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3]) → 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], x2[3] + 1)

(0) -> (1), if (x2[0] >= x0[0] && x1[0] > -1 && x0[0] > x1[0] + 1 ∧java.lang.Object(Carre(x0[0])) →^* java.lang.Object(Carre(x0[1]))∧x1[0] →^* x1[1]∧x2[0] →^* x2[1])

(1) -> (0), if (java.lang.Object(Carre(x0[1])) →^* java.lang.Object(Carre(x0[0]))∧x1[1] + 1 →^* x1[0]∧0 →^* x2[0])

(1) -> (2), if (java.lang.Object(Carre(x0[1])) →^* java.lang.Object(Carre(x0[2]))∧x1[1] + 1 →^* x1[2]∧0 →^* x2[2])

(2) -> (3), if (x2[2] > -1 && x2[2] < x0[2] ∧java.lang.Object(Carre(x0[2])) →^* java.lang.Object(Carre(x0[3]))∧x1[2] →^* x1[3]∧x2[2] →^* x2[3])

(3) -> (0), if (java.lang.Object(Carre(x0[3])) →^* java.lang.Object(Carre(x0[0]))∧x1[3] →^* x1[0]∧x2[3] + 1 →^* x2[0])

(3) -> (2), if (java.lang.Object(Carre(x0[3])) →^* java.lang.Object(Carre(x0[2]))∧x1[3] →^* x1[2]∧x2[3] + 1 →^* x2[2])

The set Q is empty.

(8) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpDefaultShapeHeuristic@44e8818b Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 1 Max Right Steps: 1

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0)), x1, x2) → COND_3352_0_IMPRIMER_GE(&&(&&(>=(x2, x0), >(x1, -1)), >(x0, +(x1, 1))), java.lang.Object(Carre(x0)), x1, x2) the following chains were created:

• We consider the chain 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), x1[0], x2[0]) → COND_3352_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0]), COND_3352_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0[1])), x1[1], x2[1]) → 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0) which results in the following constraint:
  

  (1)    (&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1)))=TRUE∧java.lang.Object(Carre(x0[0]))=java.lang.Object(Carre(x0[1]))∧x1[0]=x1[1]∧x2[0]=x2[1] ⇒ 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), x1[0], x2[0])≥NonInfC∧3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), x1[0], x2[0])≥COND_3352_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0])∧(U^Increasing(COND_3352_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0])), ≥))

  
  
  We simplified constraint (1) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (2)    (>(x0[0], +(x1[0], 1))=TRUE∧>=(x2[0], x0[0])=TRUE∧>(x1[0], -1)=TRUE ⇒ 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), x1[0], x2[0])≥NonInfC∧3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), x1[0], x2[0])≥COND_3352_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0])∧(U^Increasing(COND_3352_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0])), ≥))

  
  
  We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (3)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x2[0] + [-1]x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_3352_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0])), ≥)∧[(-2)bni_25 + (-1)Bound*bni_25] + [(-1)bni_25]x1[0] + [bni_25]x0[0] ≥ 0∧[(-1)bso_26] ≥ 0)

  
  
  We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (4)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x2[0] + [-1]x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_3352_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0])), ≥)∧[(-2)bni_25 + (-1)Bound*bni_25] + [(-1)bni_25]x1[0] + [bni_25]x0[0] ≥ 0∧[(-1)bso_26] ≥ 0)

  
  
  We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (5)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x2[0] + [-1]x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_3352_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0])), ≥)∧[(-2)bni_25 + (-1)Bound*bni_25] + [(-1)bni_25]x1[0] + [bni_25]x0[0] ≥ 0∧[(-1)bso_26] ≥ 0)

  
  
  We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (6)    (x0[0] ≥ 0∧x2[0] + [-2] + [-1]x1[0] + [-1]x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_3352_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_25] + [bni_25]x0[0] ≥ 0∧[(-1)bso_26] ≥ 0)

  
  
  We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (7)    (x0[0] ≥ 0∧x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_3352_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_25] + [bni_25]x0[0] ≥ 0∧[(-1)bso_26] ≥ 0)

  
  
  

For Pair COND_3352_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0)), x1, x2) → 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0)), +(x1, 1), 0) the following chains were created:

• We consider the chain 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), x1[0], x2[0]) → COND_3352_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0]), COND_3352_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0[1])), x1[1], x2[1]) → 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0), 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), x1[0], x2[0]) → COND_3352_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0]) which results in the following constraint:
  

  (8)    (&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1)))=TRUE∧java.lang.Object(Carre(x0[0]))=java.lang.Object(Carre(x0[1]))∧x1[0]=x1[1]∧x2[0]=x2[1]∧java.lang.Object(Carre(x0[1]))=java.lang.Object(Carre(x0[0]1))∧+(x1[1], 1)=x1[0]1∧0=x2[0]1 ⇒ COND_3352_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0[1])), x1[1], x2[1])≥NonInfC∧COND_3352_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0[1])), x1[1], x2[1])≥3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)∧(U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥))

  
  
  We simplified constraint (8) using rules (I), (II), (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (9)    (>(x0[0], +(x1[0], 1))=TRUE∧>=(x2[0], x0[0])=TRUE∧>(x1[0], -1)=TRUE ⇒ COND_3352_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0[0])), x1[0], x2[0])≥NonInfC∧COND_3352_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0[0])), x1[0], x2[0])≥3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), +(x1[0], 1), 0)∧(U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥))

  
  
  We simplified constraint (9) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (10)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x2[0] + [-1]x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥)∧[(-2)bni_27 + (-1)Bound*bni_27] + [(-1)bni_27]x1[0] + [bni_27]x0[0] ≥ 0∧[1 + (-1)bso_28] ≥ 0)

  
  
  We simplified constraint (10) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (11)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x2[0] + [-1]x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥)∧[(-2)bni_27 + (-1)Bound*bni_27] + [(-1)bni_27]x1[0] + [bni_27]x0[0] ≥ 0∧[1 + (-1)bso_28] ≥ 0)

  
  
  We simplified constraint (11) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (12)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x2[0] + [-1]x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥)∧[(-2)bni_27 + (-1)Bound*bni_27] + [(-1)bni_27]x1[0] + [bni_27]x0[0] ≥ 0∧[1 + (-1)bso_28] ≥ 0)

  
  
  We simplified constraint (12) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (13)    (x0[0] ≥ 0∧x2[0] + [-2] + [-1]x1[0] + [-1]x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥)∧[(-1)Bound*bni_27] + [bni_27]x0[0] ≥ 0∧[1 + (-1)bso_28] ≥ 0)

  
  
  We simplified constraint (13) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (14)    (x0[0] ≥ 0∧x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥)∧[(-1)Bound*bni_27] + [bni_27]x0[0] ≥ 0∧[1 + (-1)bso_28] ≥ 0)

  
  
  
• We consider the chain 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), x1[0], x2[0]) → COND_3352_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0]), COND_3352_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0[1])), x1[1], x2[1]) → 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0), 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2]) which results in the following constraint:
  

  (15)    (&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1)))=TRUE∧java.lang.Object(Carre(x0[0]))=java.lang.Object(Carre(x0[1]))∧x1[0]=x1[1]∧x2[0]=x2[1]∧java.lang.Object(Carre(x0[1]))=java.lang.Object(Carre(x0[2]))∧+(x1[1], 1)=x1[2]∧0=x2[2] ⇒ COND_3352_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0[1])), x1[1], x2[1])≥NonInfC∧COND_3352_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0[1])), x1[1], x2[1])≥3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)∧(U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥))

  
  
  We simplified constraint (15) using rules (I), (II), (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (16)    (>(x0[0], +(x1[0], 1))=TRUE∧>=(x2[0], x0[0])=TRUE∧>(x1[0], -1)=TRUE ⇒ COND_3352_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0[0])), x1[0], x2[0])≥NonInfC∧COND_3352_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0[0])), x1[0], x2[0])≥3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), +(x1[0], 1), 0)∧(U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥))

  
  
  We simplified constraint (16) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (17)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x2[0] + [-1]x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥)∧[(-2)bni_27 + (-1)Bound*bni_27] + [(-1)bni_27]x1[0] + [bni_27]x0[0] ≥ 0∧[1 + (-1)bso_28] ≥ 0)

  
  
  We simplified constraint (17) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (18)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x2[0] + [-1]x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥)∧[(-2)bni_27 + (-1)Bound*bni_27] + [(-1)bni_27]x1[0] + [bni_27]x0[0] ≥ 0∧[1 + (-1)bso_28] ≥ 0)

  
  
  We simplified constraint (18) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (19)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x2[0] + [-1]x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥)∧[(-2)bni_27 + (-1)Bound*bni_27] + [(-1)bni_27]x1[0] + [bni_27]x0[0] ≥ 0∧[1 + (-1)bso_28] ≥ 0)

  
  
  We simplified constraint (19) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (20)    (x0[0] ≥ 0∧x2[0] + [-2] + [-1]x1[0] + [-1]x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥)∧[(-1)Bound*bni_27] + [bni_27]x0[0] ≥ 0∧[1 + (-1)bso_28] ≥ 0)

  
  
  We simplified constraint (20) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (21)    (x0[0] ≥ 0∧x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥)∧[(-1)Bound*bni_27] + [bni_27]x0[0] ≥ 0∧[1 + (-1)bso_28] ≥ 0)

  
  
  

For Pair 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0)), x1, x2) → COND_3352_0_IMPRIMER_GE1(&&(>(x2, -1), <(x2, x0)), java.lang.Object(Carre(x0)), x1, x2) the following chains were created:

• We consider the chain 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2]), COND_3352_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3]) → 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1)) which results in the following constraint:
  

  (22)    (&&(>(x2[2], -1), <(x2[2], x0[2]))=TRUE∧java.lang.Object(Carre(x0[2]))=java.lang.Object(Carre(x0[3]))∧x1[2]=x1[3]∧x2[2]=x2[3] ⇒ 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2])≥NonInfC∧3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2])≥COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])∧(U^Increasing(COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥))

  
  
  We simplified constraint (22) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (23)    (>(x2[2], -1)=TRUE∧<(x2[2], x0[2])=TRUE ⇒ 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2])≥NonInfC∧3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2])≥COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])∧(U^Increasing(COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥))

  
  
  We simplified constraint (23) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (24)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥)∧[(-2)bni_29 + (-1)Bound*bni_29] + [(-1)bni_29]x1[2] + [bni_29]x0[2] ≥ 0∧[(-1)bso_30] ≥ 0)

  
  
  We simplified constraint (24) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (25)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥)∧[(-2)bni_29 + (-1)Bound*bni_29] + [(-1)bni_29]x1[2] + [bni_29]x0[2] ≥ 0∧[(-1)bso_30] ≥ 0)

  
  
  We simplified constraint (25) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (26)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥)∧[(-2)bni_29 + (-1)Bound*bni_29] + [(-1)bni_29]x1[2] + [bni_29]x0[2] ≥ 0∧[(-1)bso_30] ≥ 0)

  
  
  We simplified constraint (26) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (27)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥)∧[(-1)bni_29] = 0∧[(-2)bni_29 + (-1)Bound*bni_29] + [bni_29]x0[2] ≥ 0∧0 = 0∧[(-1)bso_30] ≥ 0)

  
  
  We simplified constraint (27) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (28)    (x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥)∧[(-1)bni_29] = 0∧[(-1)bni_29 + (-1)Bound*bni_29] + [bni_29]x2[2] + [bni_29]x0[2] ≥ 0∧0 = 0∧[(-1)bso_30] ≥ 0)

  
  
  

For Pair COND_3352_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0)), x1, x2) → 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0)), x1, +(x2, 1)) the following chains were created:

• We consider the chain 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2]), COND_3352_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3]) → 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1)), 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), x1[0], x2[0]) → COND_3352_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0]) which results in the following constraint:
  

  (29)    (&&(>(x2[2], -1), <(x2[2], x0[2]))=TRUE∧java.lang.Object(Carre(x0[2]))=java.lang.Object(Carre(x0[3]))∧x1[2]=x1[3]∧x2[2]=x2[3]∧java.lang.Object(Carre(x0[3]))=java.lang.Object(Carre(x0[0]))∧x1[3]=x1[0]∧+(x2[3], 1)=x2[0] ⇒ COND_3352_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3])≥NonInfC∧COND_3352_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3])≥3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))∧(U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥))

  
  
  We simplified constraint (29) using rules (I), (II), (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (30)    (>(x2[2], -1)=TRUE∧<(x2[2], x0[2])=TRUE ⇒ COND_3352_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[2])), x1[2], x2[2])≥NonInfC∧COND_3352_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[2])), x1[2], x2[2])≥3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], +(x2[2], 1))∧(U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥))

  
  
  We simplified constraint (30) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (31)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[(-2)bni_31 + (-1)Bound*bni_31] + [(-1)bni_31]x1[2] + [bni_31]x0[2] ≥ 0∧[(-1)bso_32] ≥ 0)

  
  
  We simplified constraint (31) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (32)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[(-2)bni_31 + (-1)Bound*bni_31] + [(-1)bni_31]x1[2] + [bni_31]x0[2] ≥ 0∧[(-1)bso_32] ≥ 0)

  
  
  We simplified constraint (32) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (33)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[(-2)bni_31 + (-1)Bound*bni_31] + [(-1)bni_31]x1[2] + [bni_31]x0[2] ≥ 0∧[(-1)bso_32] ≥ 0)

  
  
  We simplified constraint (33) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (34)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[(-1)bni_31] = 0∧[(-2)bni_31 + (-1)Bound*bni_31] + [bni_31]x0[2] ≥ 0∧0 = 0∧[(-1)bso_32] ≥ 0)

  
  
  We simplified constraint (34) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (35)    (x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[(-1)bni_31] = 0∧[(-1)bni_31 + (-1)Bound*bni_31] + [bni_31]x2[2] + [bni_31]x0[2] ≥ 0∧0 = 0∧[(-1)bso_32] ≥ 0)

  
  
  
• We consider the chain 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2]), COND_3352_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3]) → 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1)), 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2]) which results in the following constraint:
  

  (36)    (&&(>(x2[2], -1), <(x2[2], x0[2]))=TRUE∧java.lang.Object(Carre(x0[2]))=java.lang.Object(Carre(x0[3]))∧x1[2]=x1[3]∧x2[2]=x2[3]∧java.lang.Object(Carre(x0[3]))=java.lang.Object(Carre(x0[2]1))∧x1[3]=x1[2]1∧+(x2[3], 1)=x2[2]1 ⇒ COND_3352_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3])≥NonInfC∧COND_3352_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3])≥3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))∧(U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥))

  
  
  We simplified constraint (36) using rules (I), (II), (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (37)    (>(x2[2], -1)=TRUE∧<(x2[2], x0[2])=TRUE ⇒ COND_3352_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[2])), x1[2], x2[2])≥NonInfC∧COND_3352_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[2])), x1[2], x2[2])≥3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], +(x2[2], 1))∧(U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥))

  
  
  We simplified constraint (37) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (38)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[(-2)bni_31 + (-1)Bound*bni_31] + [(-1)bni_31]x1[2] + [bni_31]x0[2] ≥ 0∧[(-1)bso_32] ≥ 0)

  
  
  We simplified constraint (38) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (39)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[(-2)bni_31 + (-1)Bound*bni_31] + [(-1)bni_31]x1[2] + [bni_31]x0[2] ≥ 0∧[(-1)bso_32] ≥ 0)

  
  
  We simplified constraint (39) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (40)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[(-2)bni_31 + (-1)Bound*bni_31] + [(-1)bni_31]x1[2] + [bni_31]x0[2] ≥ 0∧[(-1)bso_32] ≥ 0)

  
  
  We simplified constraint (40) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (41)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[(-1)bni_31] = 0∧[(-2)bni_31 + (-1)Bound*bni_31] + [bni_31]x0[2] ≥ 0∧0 = 0∧[(-1)bso_32] ≥ 0)

  
  
  We simplified constraint (41) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (42)    (x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[(-1)bni_31] = 0∧[(-1)bni_31 + (-1)Bound*bni_31] + [bni_31]x2[2] + [bni_31]x0[2] ≥ 0∧0 = 0∧[(-1)bso_32] ≥ 0)

  
  
  

To summarize, we get the following constraints P_≥ for the following pairs.

• 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0)), x1, x2) → COND_3352_0_IMPRIMER_GE(&&(&&(>=(x2, x0), >(x1, -1)), >(x0, +(x1, 1))), java.lang.Object(Carre(x0)), x1, x2)
  
  • (x0[0] ≥ 0∧x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_3352_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_25] + [bni_25]x0[0] ≥ 0∧[(-1)bso_26] ≥ 0)
    
  
  
• COND_3352_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0)), x1, x2) → 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0)), +(x1, 1), 0)
  
  • (x0[0] ≥ 0∧x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥)∧[(-1)Bound*bni_27] + [bni_27]x0[0] ≥ 0∧[1 + (-1)bso_28] ≥ 0)
    
  • (x0[0] ≥ 0∧x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥)∧[(-1)Bound*bni_27] + [bni_27]x0[0] ≥ 0∧[1 + (-1)bso_28] ≥ 0)
    
  
  
• 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0)), x1, x2) → COND_3352_0_IMPRIMER_GE1(&&(>(x2, -1), <(x2, x0)), java.lang.Object(Carre(x0)), x1, x2)
  
  • (x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥)∧[(-1)bni_29] = 0∧[(-1)bni_29 + (-1)Bound*bni_29] + [bni_29]x2[2] + [bni_29]x0[2] ≥ 0∧0 = 0∧[(-1)bso_30] ≥ 0)
    
  
  
• COND_3352_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0)), x1, x2) → 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0)), x1, +(x2, 1))
  
  • (x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[(-1)bni_31] = 0∧[(-1)bni_31 + (-1)Bound*bni_31] + [bni_31]x2[2] + [bni_31]x0[2] ≥ 0∧0 = 0∧[(-1)bso_32] ≥ 0)
    
  • (x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[(-1)bni_31] = 0∧[(-1)bni_31 + (-1)Bound*bni_31] + [bni_31]x2[2] + [bni_31]x0[2] ≥ 0∧0 = 0∧[(-1)bso_32] ≥ 0)
    
  
  

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0   
POL(FALSE) = [2]   
POL(3352_0_IMPRIMER_GE(x₁, x₂, x₃)) = [-1] + [-1]x₂ + [-1]x₁   
POL(java.lang.Object(x₁)) = [2] + x₁   
POL(Carre(x₁)) = [-1] + [-1]x₁   
POL(COND_3352_0_IMPRIMER_GE(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃ + [-1]x₂   
POL(&&(x₁, x₂)) = [-1]   
POL(>=(x₁, x₂)) = [-1]   
POL(>(x₁, x₂)) = [-1]   
POL(-1) = [-1]   
POL(+(x₁, x₂)) = x₁ + x₂   
POL(1) = [1]   
POL(0) = 0   
POL(COND_3352_0_IMPRIMER_GE1(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃ + [-1]x₂   
POL(<(x₁, x₂)) = [-1]   

The following pairs are in P_>:

COND_3352_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0[1])), x1[1], x2[1]) → 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)

The following pairs are in P_bound:

3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), x1[0], x2[0]) → COND_3352_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0])
COND_3352_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0[1])), x1[1], x2[1]) → 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)

The following pairs are in P_≥:

3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), x1[0], x2[0]) → COND_3352_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0])
3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])
COND_3352_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3]) → 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))

There are no usable rules.

(9) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
||	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), x1[0], x2[0]) → COND_3352_0_IMPRIMER_GE(x2[0] >= x0[0] && x1[0] > -1 && x0[0] > x1[0] + 1, java.lang.Object(Carre(x0[0])), x1[0], x2[0])
(2): 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_3352_0_IMPRIMER_GE1(x2[2] > -1 && x2[2] < x0[2], java.lang.Object(Carre(x0[2])), x1[2], x2[2])
(3): COND_3352_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3]) → 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], x2[3] + 1)

(3) -> (0), if (java.lang.Object(Carre(x0[3])) →^* java.lang.Object(Carre(x0[0]))∧x1[3] →^* x1[0]∧x2[3] + 1 →^* x2[0])

(3) -> (2), if (java.lang.Object(Carre(x0[3])) →^* java.lang.Object(Carre(x0[2]))∧x1[3] →^* x1[2]∧x2[3] + 1 →^* x2[2])

(2) -> (3), if (x2[2] > -1 && x2[2] < x0[2] ∧java.lang.Object(Carre(x0[2])) →^* java.lang.Object(Carre(x0[3]))∧x1[2] →^* x1[3]∧x2[2] →^* x2[3])

The set Q is empty.

(10) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(11) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
||	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(3): COND_3352_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3]) → 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], x2[3] + 1)
(2): 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_3352_0_IMPRIMER_GE1(x2[2] > -1 && x2[2] < x0[2], java.lang.Object(Carre(x0[2])), x1[2], x2[2])

(3) -> (2), if (java.lang.Object(Carre(x0[3])) →^* java.lang.Object(Carre(x0[2]))∧x1[3] →^* x1[2]∧x2[3] + 1 →^* x2[2])

(2) -> (3), if (x2[2] > -1 && x2[2] < x0[2] ∧java.lang.Object(Carre(x0[2])) →^* java.lang.Object(Carre(x0[3]))∧x1[2] →^* x1[3]∧x2[2] →^* x2[3])

The set Q is empty.

(12) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpDefaultShapeHeuristic@44e8818b Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 1 Max Right Steps: 1

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair COND_3352_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3]) → 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1)) the following chains were created:

• We consider the chain 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2]), COND_3352_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3]) → 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1)), 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2]) which results in the following constraint:
  

  (1)    (&&(>(x2[2], -1), <(x2[2], x0[2]))=TRUE∧java.lang.Object(Carre(x0[2]))=java.lang.Object(Carre(x0[3]))∧x1[2]=x1[3]∧x2[2]=x2[3]∧java.lang.Object(Carre(x0[3]))=java.lang.Object(Carre(x0[2]1))∧x1[3]=x1[2]1∧+(x2[3], 1)=x2[2]1 ⇒ COND_3352_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3])≥NonInfC∧COND_3352_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3])≥3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))∧(U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥))

  
  
  We simplified constraint (1) using rules (I), (II), (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (2)    (>(x2[2], -1)=TRUE∧<(x2[2], x0[2])=TRUE ⇒ COND_3352_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[2])), x1[2], x2[2])≥NonInfC∧COND_3352_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[2])), x1[2], x2[2])≥3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], +(x2[2], 1))∧(U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥))

  
  
  We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (3)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[(-1)Bound*bni_19] + [(-1)bni_19]x2[2] + [bni_19]x0[2] ≥ 0∧[(-1)bso_20] ≥ 0)

  
  
  We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (4)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[(-1)Bound*bni_19] + [(-1)bni_19]x2[2] + [bni_19]x0[2] ≥ 0∧[(-1)bso_20] ≥ 0)

  
  
  We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (5)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[(-1)Bound*bni_19] + [(-1)bni_19]x2[2] + [bni_19]x0[2] ≥ 0∧[(-1)bso_20] ≥ 0)

  
  
  We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (6)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧0 = 0∧[(-1)Bound*bni_19] + [(-1)bni_19]x2[2] + [bni_19]x0[2] ≥ 0∧0 = 0∧[(-1)bso_20] ≥ 0)

  
  
  We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (7)    (x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧0 = 0∧[(-1)Bound*bni_19 + bni_19] + [bni_19]x0[2] ≥ 0∧0 = 0∧[(-1)bso_20] ≥ 0)

  
  
  

For Pair 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2]) the following chains were created:

• We consider the chain 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2]), COND_3352_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3]) → 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1)) which results in the following constraint:
  

  (8)    (&&(>(x2[2], -1), <(x2[2], x0[2]))=TRUE∧java.lang.Object(Carre(x0[2]))=java.lang.Object(Carre(x0[3]))∧x1[2]=x1[3]∧x2[2]=x2[3] ⇒ 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2])≥NonInfC∧3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2])≥COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])∧(U^Increasing(COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥))

  
  
  We simplified constraint (8) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (9)    (>(x2[2], -1)=TRUE∧<(x2[2], x0[2])=TRUE ⇒ 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2])≥NonInfC∧3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2])≥COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])∧(U^Increasing(COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥))

  
  
  We simplified constraint (9) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (10)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥)∧[bni_21 + (-1)Bound*bni_21] + [(-1)bni_21]x2[2] + [bni_21]x0[2] ≥ 0∧[1 + (-1)bso_22] ≥ 0)

  
  
  We simplified constraint (10) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (11)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥)∧[bni_21 + (-1)Bound*bni_21] + [(-1)bni_21]x2[2] + [bni_21]x0[2] ≥ 0∧[1 + (-1)bso_22] ≥ 0)

  
  
  We simplified constraint (11) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (12)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥)∧[bni_21 + (-1)Bound*bni_21] + [(-1)bni_21]x2[2] + [bni_21]x0[2] ≥ 0∧[1 + (-1)bso_22] ≥ 0)

  
  
  We simplified constraint (12) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (13)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥)∧0 = 0∧[bni_21 + (-1)Bound*bni_21] + [(-1)bni_21]x2[2] + [bni_21]x0[2] ≥ 0∧0 = 0∧[1 + (-1)bso_22] ≥ 0)

  
  
  We simplified constraint (13) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (14)    (x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥)∧0 = 0∧[(2)bni_21 + (-1)Bound*bni_21] + [bni_21]x0[2] ≥ 0∧0 = 0∧[1 + (-1)bso_22] ≥ 0)

  
  
  

To summarize, we get the following constraints P_≥ for the following pairs.

• COND_3352_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3]) → 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))
  
  • (x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧0 = 0∧[(-1)Bound*bni_19 + bni_19] + [bni_19]x0[2] ≥ 0∧0 = 0∧[(-1)bso_20] ≥ 0)
    
  
  
• 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])
  
  • (x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥)∧0 = 0∧[(2)bni_21 + (-1)Bound*bni_21] + [bni_21]x0[2] ≥ 0∧0 = 0∧[1 + (-1)bso_22] ≥ 0)
    
  
  

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = [1]   
POL(FALSE) = [2]   
POL(COND_3352_0_IMPRIMER_GE1(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₄ + [-1]x₂ + [-1]x₁   
POL(java.lang.Object(x₁)) = [-1] + x₁   
POL(Carre(x₁)) = [-1] + [-1]x₁   
POL(3352_0_IMPRIMER_GE(x₁, x₂, x₃)) = [-1] + [-1]x₃ + [-1]x₁   
POL(+(x₁, x₂)) = x₁ + x₂   
POL(1) = [1]   
POL(&&(x₁, x₂)) = [1]   
POL(>(x₁, x₂)) = [-1]   
POL(-1) = [-1]   
POL(<(x₁, x₂)) = [-1]   

The following pairs are in P_>:

3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])

The following pairs are in P_bound:

COND_3352_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3]) → 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))
3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_3352_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])

The following pairs are in P_≥:

COND_3352_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3]) → 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))

At least the following rules have been oriented under context sensitive arithmetic replacement:

&&(TRUE, TRUE)¹ ↔ TRUE¹
FALSE¹ → &&(TRUE, FALSE)¹
FALSE¹ → &&(FALSE, TRUE)¹
FALSE¹ → &&(FALSE, FALSE)¹

(13) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
||	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(3): COND_3352_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3]) → 3352_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], x2[3] + 1)


The set Q is empty.

(14) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(15) TRUE

(16) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Carre.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses: UsedFieldsAnalysis

(17) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 32 rules for P and 0 rules for R.

P rules:
1911_0_init_ConstantStackPush(EOS(STATIC_1911), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i253, i253) → 1919_0_init_GE(EOS(STATIC_1919), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i253, i253, 3)
1919_0_init_GE(EOS(STATIC_1919), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i263, matching1) → 1921_0_init_GE(EOS(STATIC_1921), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i263, 3) | =(matching1, 3)
1921_0_init_GE(EOS(STATIC_1921), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i263, matching1) → 1925_0_init_ConstantStackPush(EOS(STATIC_1925), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263) | &&(<(i263, 3), =(matching1, 3))
1925_0_init_ConstantStackPush(EOS(STATIC_1925), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263) → 1930_0_init_Store(EOS(STATIC_1930), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, 0)
1930_0_init_Store(EOS(STATIC_1930), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, matching1) → 1934_0_init_Load(EOS(STATIC_1934), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, 0) | =(matching1, 0)
1934_0_init_Load(EOS(STATIC_1934), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, matching1) → 2047_0_init_Load(EOS(STATIC_2047), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, 0) | =(matching1, 0)
2047_0_init_Load(EOS(STATIC_2047), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i286) → 2144_0_init_Load(EOS(STATIC_2144), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i286)
2144_0_init_Load(EOS(STATIC_2144), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i309) → 2254_0_init_Load(EOS(STATIC_2254), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i309)
2254_0_init_Load(EOS(STATIC_2254), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i338) → 2260_0_init_ConstantStackPush(EOS(STATIC_2260), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i338, i338)
2260_0_init_ConstantStackPush(EOS(STATIC_2260), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i338, i338) → 2268_0_init_GE(EOS(STATIC_2268), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i338, i338, 3)
2268_0_init_GE(EOS(STATIC_2268), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i348, i348, matching1) → 2277_0_init_GE(EOS(STATIC_2277), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i348, i348, 3) | =(matching1, 3)
2268_0_init_GE(EOS(STATIC_2268), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, matching1, matching2, matching3) → 2279_0_init_GE(EOS(STATIC_2279), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, 3, 3, 3) | &&(&&(=(matching1, 3), =(matching2, 3)), =(matching3, 3))
2277_0_init_GE(EOS(STATIC_2277), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i348, i348, matching1) → 2282_0_init_Load(EOS(STATIC_2282), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i348) | &&(<(i348, 3), =(matching1, 3))
2282_0_init_Load(EOS(STATIC_2282), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i348) → 2287_0_init_FieldAccess(EOS(STATIC_2287), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i348, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))))
2287_0_init_FieldAccess(EOS(STATIC_2287), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i348, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27))))) → 2292_0_init_Load(EOS(STATIC_2292), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i348, java.lang.Object(ARRAY(i27)))
2292_0_init_Load(EOS(STATIC_2292), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i348, java.lang.Object(ARRAY(i27))) → 2309_0_init_ArrayAccess(EOS(STATIC_2309), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i348, java.lang.Object(ARRAY(i27)), i263)
2309_0_init_ArrayAccess(EOS(STATIC_2309), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i348, java.lang.Object(ARRAY(i27)), i263) → 2457_0_init_ArrayAccess(EOS(STATIC_2457), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i348, java.lang.Object(ARRAY(i27)), i263)
2457_0_init_ArrayAccess(EOS(STATIC_2457), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i348, java.lang.Object(ARRAY(i27)), i263) → 2461_0_init_Load(EOS(STATIC_2461), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i348, o1687) | <(i263, i27)
2461_0_init_Load(EOS(STATIC_2461), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i348, o1687) → 2465_0_init_ConstantStackPush(EOS(STATIC_2465), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i348, o1687, i348)
2465_0_init_ConstantStackPush(EOS(STATIC_2465), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i348, o1687, i348) → 2468_0_init_ArrayAccess(EOS(STATIC_2468), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i348, o1687, i348, 0)
2468_0_init_ArrayAccess(EOS(STATIC_2468), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i348, java.lang.Object(o1696put), i348, matching1) → 2473_0_init_ArrayAccess(EOS(STATIC_2473), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i348, java.lang.Object(o1696put), i348, 0) | =(matching1, 0)
2473_0_init_ArrayAccess(EOS(STATIC_2473), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i348, java.lang.Object(ARRAY(i392)), i348, matching1) → 2478_0_init_ArrayAccess(EOS(STATIC_2478), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i348, java.lang.Object(ARRAY(i392)), i348, 0) | &&(>=(i392, 0), =(matching1, 0))
2478_0_init_ArrayAccess(EOS(STATIC_2478), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i348, java.lang.Object(ARRAY(i392)), i348, matching1) → 2482_0_init_ArrayAccess(EOS(STATIC_2482), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i348, java.lang.Object(ARRAY(i392)), i348, 0) | =(matching1, 0)
2482_0_init_ArrayAccess(EOS(STATIC_2482), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i348, java.lang.Object(ARRAY(i392)), i348, matching1) → 2494_0_init_Inc(EOS(STATIC_2494), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i348) | &&(<(i348, i392), =(matching1, 0))
2494_0_init_Inc(EOS(STATIC_2494), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i348) → 2499_0_init_JMP(EOS(STATIC_2499), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, +(i348, 1)) | >=(i348, 0)
2499_0_init_JMP(EOS(STATIC_2499), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i395) → 2506_0_init_Load(EOS(STATIC_2506), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i395)
2506_0_init_Load(EOS(STATIC_2506), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i395) → 2254_0_init_Load(EOS(STATIC_2254), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, i395)
2279_0_init_GE(EOS(STATIC_2279), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263, matching1, matching2, matching3) → 2284_0_init_Inc(EOS(STATIC_2284), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263) | &&(&&(=(matching1, 3), =(matching2, 3)), =(matching3, 3))
2284_0_init_Inc(EOS(STATIC_2284), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i263) → 2289_0_init_JMP(EOS(STATIC_2289), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), +(i263, 1)) | >=(i263, 0)
2289_0_init_JMP(EOS(STATIC_2289), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i349) → 2301_0_init_Load(EOS(STATIC_2301), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i349)
2301_0_init_Load(EOS(STATIC_2301), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i349) → 1908_0_init_Load(EOS(STATIC_1908), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i349)
1908_0_init_Load(EOS(STATIC_1908), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i253) → 1911_0_init_ConstantStackPush(EOS(STATIC_1911), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i253, i253)
R rules:

Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.

P rules:
2268_0_init_GE(EOS(STATIC_2268), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(x0)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(x0)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(x0)))), x1, x2, x2, 3) → 2268_0_init_GE(EOS(STATIC_2268), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(x0)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(x0)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(x0)))), x1, +(x2, 1), +(x2, 1), 3) | &&(&&(>(+(x2, 1), 0), <(x2, 3)), <(x1, x0))
2268_0_init_GE(EOS(STATIC_2268), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(x0)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(x0)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(x0)))), x1, 3, 3, 3) → 2268_0_init_GE(EOS(STATIC_2268), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(x0)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(x0)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(x0)))), +(x1, 1), 0, 0, 3) | &&(>(+(x1, 1), 0), <(x1, 2))
R rules:

Filtered ground terms:

2268_0_init_GE(x1, x2, x3, x4, x5, x6, x7, x8) → 2268_0_init_GE(x2, x3, x4, x5, x6, x7)
Carre(x1, x2) → Carre(x2)
EOS(x1) → EOS
Cond_2268_0_init_GE1(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_2268_0_init_GE1(x1, x3, x4, x5, x6)
Cond_2268_0_init_GE(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_2268_0_init_GE(x1, x3, x4, x5, x6, x7, x8)

Filtered duplicate args:

2268_0_init_GE(x1, x2, x3, x4, x5, x6) → 2268_0_init_GE(x3, x4, x6)
Cond_2268_0_init_GE(x1, x2, x3, x4, x5, x6, x7) → Cond_2268_0_init_GE(x1, x4, x5, x7)
Cond_2268_0_init_GE1(x1, x2, x3, x4, x5) → Cond_2268_0_init_GE1(x1, x4, x5)

Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.

P rules:
2268_0_init_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, x2) → 2268_0_init_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, +(x2, 1)) | &&(&&(>(x2, -1), <(x2, 3)), <(x1, x0))
2268_0_init_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, 3) → 2268_0_init_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), +(x1, 1), 0) | &&(>(x1, -1), <(x1, 2))
R rules:

Finished conversion. Obtained 4 rules for P and 0 rules for R. System has predefined symbols.

P rules:
2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, x2) → COND_2268_0_INIT_GE(&&(&&(>(x2, -1), <(x2, 3)), <(x1, x0)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, x2)
COND_2268_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, x2) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, +(x2, 1))
2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, 3) → COND_2268_0_INIT_GE1(&&(>(x1, -1), <(x1, 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, 3)
COND_2268_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, 3) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), +(x1, 1), 0)
R rules:

(18) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
||	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0]) → COND_2268_0_INIT_GE(x2[0] > -1 && x2[0] < 3 && x1[0] < x0[0], java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])
(1): COND_2268_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1]) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1] + 1)
(2): 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3) → COND_2268_0_INIT_GE1(x1[2] > -1 && x1[2] < 2, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)
(3): COND_2268_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3] + 1, 0)

(0) -> (1), if (x2[0] > -1 && x2[0] < 3 && x1[0] < x0[0] ∧java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1]))))∧x1[0] →^* x1[1]∧x2[0] →^* x2[1])

(1) -> (0), if (java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0]))))∧x1[1] →^* x1[0]∧x2[1] + 1 →^* x2[0])

(1) -> (2), if (java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2]))))∧x1[1] →^* x1[2]∧x2[1] + 1 →^* 3)

(2) -> (3), if (x1[2] > -1 && x1[2] < 2 ∧java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3]))))∧x1[2] →^* x1[3])

(3) -> (0), if (java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0]))))∧x1[3] + 1 →^* x1[0]∧0 →^* x2[0])

(3) -> (2), if (java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2]))))∧x1[3] + 1 →^* x1[2]∧0 →^* 3)

The set Q is empty.

(19) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpCand1ShapeHeuristic@40eff50 Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 0 Max Right Steps: 0

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, x2) → COND_2268_0_INIT_GE(&&(&&(>(x2, -1), <(x2, 3)), <(x1, x0)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, x2) the following chains were created:

• We consider the chain 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0]) → COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0]), COND_2268_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1]) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1)) which results in the following constraint:
  

  (1)    (&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0]))=TRUE∧java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0]))))=java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1]))))∧x1[0]=x1[1]∧x2[0]=x2[1] ⇒ 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])≥NonInfC∧2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])≥COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])∧(U^Increasing(COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥))

  
  
  We simplified constraint (1) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (2)    (<(x1[0], x0[0])=TRUE∧>(x2[0], -1)=TRUE∧<(x2[0], 3)=TRUE ⇒ 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])≥NonInfC∧2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])≥COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])∧(U^Increasing(COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥))

  
  
  We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (3)    (x0[0] + [-1] + [-1]x1[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0 ⇒ (U^Increasing(COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)bni_12 + (-1)Bound*bni_12] + [(-1)bni_12]x1[0] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)

  
  
  We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (4)    (x0[0] + [-1] + [-1]x1[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0 ⇒ (U^Increasing(COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)bni_12 + (-1)Bound*bni_12] + [(-1)bni_12]x1[0] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)

  
  
  We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (5)    (x0[0] + [-1] + [-1]x1[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0 ⇒ (U^Increasing(COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)bni_12 + (-1)Bound*bni_12] + [(-1)bni_12]x1[0] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)

  
  
  We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (6)    (x0[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0 ⇒ (U^Increasing(COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)

  
  
  We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (7)    (x0[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)

  
  

  (8)    (x0[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)

  
  
  

For Pair COND_2268_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, x2) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, +(x2, 1)) the following chains were created:

• We consider the chain COND_2268_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1]) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1)) which results in the following constraint:
  

  (9)    (COND_2268_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1])≥NonInfC∧COND_2268_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1])≥2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))∧(U^Increasing(2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))), ≥))

  
  
  We simplified constraint (9) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (10)    ((U^Increasing(2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))), ≥)∧[bni_14] = 0∧[(-1)bso_15] ≥ 0)

  
  
  We simplified constraint (10) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (11)    ((U^Increasing(2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))), ≥)∧[bni_14] = 0∧[(-1)bso_15] ≥ 0)

  
  
  We simplified constraint (11) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (12)    ((U^Increasing(2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))), ≥)∧[bni_14] = 0∧[(-1)bso_15] ≥ 0)

  
  
  We simplified constraint (12) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (13)    ((U^Increasing(2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))), ≥)∧[bni_14] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_15] ≥ 0)

  
  
  

For Pair 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, 3) → COND_2268_0_INIT_GE1(&&(>(x1, -1), <(x1, 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, 3) the following chains were created:

• We consider the chain 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3) → COND_2268_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3), COND_2268_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0) which results in the following constraint:
  

  (14)    (&&(>(x1[2], -1), <(x1[2], 2))=TRUE∧java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2]))))=java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3]))))∧x1[2]=x1[3] ⇒ 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)≥NonInfC∧2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)≥COND_2268_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)∧(U^Increasing(COND_2268_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)), ≥))

  
  
  We simplified constraint (14) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (15)    (>(x1[2], -1)=TRUE∧<(x1[2], 2)=TRUE ⇒ 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)≥NonInfC∧2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)≥COND_2268_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)∧(U^Increasing(COND_2268_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)), ≥))

  
  
  We simplified constraint (15) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (16)    (x1[2] ≥ 0∧[1] + [-1]x1[2] ≥ 0 ⇒ (U^Increasing(COND_2268_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)), ≥)∧[(-1)bni_16 + (-1)Bound*bni_16] + [(-1)bni_16]x1[2] + [bni_16]x0[2] ≥ 0∧[(-1)bso_17] ≥ 0)

  
  
  We simplified constraint (16) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (17)    (x1[2] ≥ 0∧[1] + [-1]x1[2] ≥ 0 ⇒ (U^Increasing(COND_2268_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)), ≥)∧[(-1)bni_16 + (-1)Bound*bni_16] + [(-1)bni_16]x1[2] + [bni_16]x0[2] ≥ 0∧[(-1)bso_17] ≥ 0)

  
  
  We simplified constraint (17) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (18)    (x1[2] ≥ 0∧[1] + [-1]x1[2] ≥ 0 ⇒ (U^Increasing(COND_2268_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)), ≥)∧[(-1)bni_16 + (-1)Bound*bni_16] + [(-1)bni_16]x1[2] + [bni_16]x0[2] ≥ 0∧[(-1)bso_17] ≥ 0)

  
  
  We simplified constraint (18) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (19)    (x1[2] ≥ 0∧[1] + [-1]x1[2] ≥ 0 ⇒ (U^Increasing(COND_2268_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)), ≥)∧[bni_16] = 0∧[(-1)bni_16 + (-1)Bound*bni_16] + [(-1)bni_16]x1[2] ≥ 0∧0 = 0∧[(-1)bso_17] ≥ 0)

  
  
  

For Pair COND_2268_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, 3) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), +(x1, 1), 0) the following chains were created:

• We consider the chain COND_2268_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0) which results in the following constraint:
  

  (20)    (COND_2268_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3)≥NonInfC∧COND_2268_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3)≥2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)∧(U^Increasing(2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)), ≥))

  
  
  We simplified constraint (20) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (21)    ((U^Increasing(2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)), ≥)∧[bni_18] = 0∧[1 + (-1)bso_19] ≥ 0)

  
  
  We simplified constraint (21) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (22)    ((U^Increasing(2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)), ≥)∧[bni_18] = 0∧[1 + (-1)bso_19] ≥ 0)

  
  
  We simplified constraint (22) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (23)    ((U^Increasing(2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)), ≥)∧[bni_18] = 0∧[1 + (-1)bso_19] ≥ 0)

  
  
  We simplified constraint (23) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (24)    ((U^Increasing(2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)), ≥)∧[bni_18] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_19] ≥ 0)

  
  
  

To summarize, we get the following constraints P_≥ for the following pairs.

• 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, x2) → COND_2268_0_INIT_GE(&&(&&(>(x2, -1), <(x2, 3)), <(x1, x0)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, x2)
  
  • (x0[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)
    
  • (x0[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)
    
  
  
• COND_2268_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, x2) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, +(x2, 1))
  
  • ((U^Increasing(2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))), ≥)∧[bni_14] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_15] ≥ 0)
    
  
  
• 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, 3) → COND_2268_0_INIT_GE1(&&(>(x1, -1), <(x1, 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, 3)
  
  • (x1[2] ≥ 0∧[1] + [-1]x1[2] ≥ 0 ⇒ (U^Increasing(COND_2268_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)), ≥)∧[bni_16] = 0∧[(-1)bni_16 + (-1)Bound*bni_16] + [(-1)bni_16]x1[2] ≥ 0∧0 = 0∧[(-1)bso_17] ≥ 0)
    
  
  
• COND_2268_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, 3) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), +(x1, 1), 0)
  
  • ((U^Increasing(2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)), ≥)∧[bni_18] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_19] ≥ 0)
    
  
  

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0   
POL(FALSE) = 0   
POL(2268_0_INIT_GE(x₁, x₂, x₃)) = [-1] + [-1]x₂ + x₁   
POL(java.lang.Object(x₁)) = x₁   
POL(Carre(x₁)) = x₁   
POL(ARRAY(x₁)) = x₁   
POL(COND_2268_0_INIT_GE(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃ + x₂   
POL(&&(x₁, x₂)) = [-1]   
POL(>(x₁, x₂)) = [-1]   
POL(-1) = [-1]   
POL(<(x₁, x₂)) = [-1]   
POL(3) = [3]   
POL(+(x₁, x₂)) = x₁ + x₂   
POL(1) = [1]   
POL(COND_2268_0_INIT_GE1(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃ + x₂   
POL(2) = [2]   
POL(0) = 0   

The following pairs are in P_>:

COND_2268_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)

The following pairs are in P_bound:

2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0]) → COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])

The following pairs are in P_≥:

2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0]) → COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])
COND_2268_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1]) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))
2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3) → COND_2268_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)

There are no usable rules.

(20) Complex Obligation (AND)

(21) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
||	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0]) → COND_2268_0_INIT_GE(x2[0] > -1 && x2[0] < 3 && x1[0] < x0[0], java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])
(1): COND_2268_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1]) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1] + 1)
(2): 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3) → COND_2268_0_INIT_GE1(x1[2] > -1 && x1[2] < 2, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)

(1) -> (0), if (java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0]))))∧x1[1] →^* x1[0]∧x2[1] + 1 →^* x2[0])

(0) -> (1), if (x2[0] > -1 && x2[0] < 3 && x1[0] < x0[0] ∧java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1]))))∧x1[0] →^* x1[1]∧x2[0] →^* x2[1])

(1) -> (2), if (java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2]))))∧x1[1] →^* x1[2]∧x2[1] + 1 →^* 3)

The set Q is empty.

(22) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(23) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
||	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_2268_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1]) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1] + 1)
(0): 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0]) → COND_2268_0_INIT_GE(x2[0] > -1 && x2[0] < 3 && x1[0] < x0[0], java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])

(1) -> (0), if (java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0]))))∧x1[1] →^* x1[0]∧x2[1] + 1 →^* x2[0])

(0) -> (1), if (x2[0] > -1 && x2[0] < 3 && x1[0] < x0[0] ∧java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1]))))∧x1[0] →^* x1[1]∧x2[0] →^* x2[1])

The set Q is empty.

(24) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpCand1ShapeHeuristic@40eff50 Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 0 Max Right Steps: 0

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair COND_2268_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1]) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1)) the following chains were created:

• We consider the chain COND_2268_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1]) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1)) which results in the following constraint:
  

  (1)    (COND_2268_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1])≥NonInfC∧COND_2268_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1])≥2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))∧(U^Increasing(2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))), ≥))

  
  
  We simplified constraint (1) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (2)    ((U^Increasing(2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))), ≥)∧[bni_10] = 0∧[1 + (-1)bso_11] ≥ 0)

  
  
  We simplified constraint (2) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (3)    ((U^Increasing(2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))), ≥)∧[bni_10] = 0∧[1 + (-1)bso_11] ≥ 0)

  
  
  We simplified constraint (3) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (4)    ((U^Increasing(2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))), ≥)∧[bni_10] = 0∧[1 + (-1)bso_11] ≥ 0)

  
  
  We simplified constraint (4) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (5)    ((U^Increasing(2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))), ≥)∧[bni_10] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_11] ≥ 0)

  
  
  

For Pair 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0]) → COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0]) the following chains were created:

• We consider the chain 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0]) → COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0]), COND_2268_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1]) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1)) which results in the following constraint:
  

  (6)    (&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0]))=TRUE∧java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0]))))=java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1]))))∧x1[0]=x1[1]∧x2[0]=x2[1] ⇒ 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])≥NonInfC∧2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])≥COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])∧(U^Increasing(COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥))

  
  
  We simplified constraint (6) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (7)    (<(x1[0], x0[0])=TRUE∧>(x2[0], -1)=TRUE∧<(x2[0], 3)=TRUE ⇒ 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])≥NonInfC∧2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])≥COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])∧(U^Increasing(COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥))

  
  
  We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (8)    (x0[0] + [-1] + [-1]x1[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0 ⇒ (U^Increasing(COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)bni_12 + (-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [(-1)bni_12]x1[0] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)

  
  
  We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (9)    (x0[0] + [-1] + [-1]x1[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0 ⇒ (U^Increasing(COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)bni_12 + (-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [(-1)bni_12]x1[0] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)

  
  
  We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (10)    (x0[0] + [-1] + [-1]x1[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0 ⇒ (U^Increasing(COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)bni_12 + (-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [(-1)bni_12]x1[0] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)

  
  
  We simplified constraint (10) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (11)    (x0[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0 ⇒ (U^Increasing(COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)

  
  
  We simplified constraint (11) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (12)    (x0[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)

  
  

  (13)    (x0[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)

  
  
  

To summarize, we get the following constraints P_≥ for the following pairs.

• COND_2268_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1]) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))
  
  • ((U^Increasing(2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))), ≥)∧[bni_10] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_11] ≥ 0)
    
  
  
• 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0]) → COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])
  
  • (x0[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)
    
  • (x0[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)
    
  
  

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0   
POL(FALSE) = 0   
POL(COND_2268_0_INIT_GE(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃ + x₂ + [-1]x₄   
POL(java.lang.Object(x₁)) = x₁   
POL(Carre(x₁)) = x₁   
POL(ARRAY(x₁)) = x₁   
POL(2268_0_INIT_GE(x₁, x₂, x₃)) = [-1] + [-1]x₃ + [-1]x₂ + x₁   
POL(+(x₁, x₂)) = x₁ + x₂   
POL(1) = [1]   
POL(&&(x₁, x₂)) = [-1]   
POL(>(x₁, x₂)) = [-1]   
POL(-1) = [-1]   
POL(<(x₁, x₂)) = [-1]   
POL(3) = [3]   

The following pairs are in P_>:

COND_2268_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1]) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))

The following pairs are in P_bound:

2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0]) → COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])

The following pairs are in P_≥:

2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0]) → COND_2268_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])

There are no usable rules.

(25) Complex Obligation (AND)

(26) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
||	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0]) → COND_2268_0_INIT_GE(x2[0] > -1 && x2[0] < 3 && x1[0] < x0[0], java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])


The set Q is empty.

(27) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(28) TRUE

(29) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
||	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_2268_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1]) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1] + 1)


The set Q is empty.

(30) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(31) TRUE

(32) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
||	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_2268_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1]) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1] + 1)
(2): 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3) → COND_2268_0_INIT_GE1(x1[2] > -1 && x1[2] < 2, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)
(3): COND_2268_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3] + 1, 0)

(1) -> (2), if (java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2]))))∧x1[1] →^* x1[2]∧x2[1] + 1 →^* 3)

(3) -> (2), if (java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2]))))∧x1[3] + 1 →^* x1[2]∧0 →^* 3)

(2) -> (3), if (x1[2] > -1 && x1[2] < 2 ∧java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3]))))∧x1[2] →^* x1[3])

The set Q is empty.

(33) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(34) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
||	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(3): COND_2268_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3] + 1, 0)
(2): 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3) → COND_2268_0_INIT_GE1(x1[2] > -1 && x1[2] < 2, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)

(3) -> (2), if (java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2]))))∧x1[3] + 1 →^* x1[2]∧0 →^* 3)

(2) -> (3), if (x1[2] > -1 && x1[2] < 2 ∧java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3]))))∧x1[2] →^* x1[3])

The set Q is empty.

(35) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpCand1ShapeHeuristic@40eff50 Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 0 Max Right Steps: 0

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair COND_2268_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0) the following chains were created:

• We consider the chain COND_2268_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0) which results in the following constraint:
  

  (1)    (COND_2268_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3)≥NonInfC∧COND_2268_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3)≥2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)∧(U^Increasing(2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)), ≥))

  
  
  We simplified constraint (1) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (2)    ((U^Increasing(2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)), ≥)∧[bni_12] = 0∧[1 + (-1)bso_13] ≥ 0)

  
  
  We simplified constraint (2) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (3)    ((U^Increasing(2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)), ≥)∧[bni_12] = 0∧[1 + (-1)bso_13] ≥ 0)

  
  
  We simplified constraint (3) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (4)    ((U^Increasing(2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)), ≥)∧[bni_12] = 0∧[1 + (-1)bso_13] ≥ 0)

  
  
  We simplified constraint (4) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (5)    ((U^Increasing(2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)), ≥)∧[bni_12] = 0∧0 = 0∧[1 + (-1)bso_13] ≥ 0)

  
  
  

For Pair 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3) → COND_2268_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3) the following chains were created:

• We consider the chain 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3) → COND_2268_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3), COND_2268_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0) which results in the following constraint:
  

  (6)    (&&(>(x1[2], -1), <(x1[2], 2))=TRUE∧java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2]))))=java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3]))))∧x1[2]=x1[3] ⇒ 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)≥NonInfC∧2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)≥COND_2268_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)∧(U^Increasing(COND_2268_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)), ≥))

  
  
  We simplified constraint (6) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (7)    (>(x1[2], -1)=TRUE∧<(x1[2], 2)=TRUE ⇒ 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)≥NonInfC∧2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)≥COND_2268_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)∧(U^Increasing(COND_2268_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)), ≥))

  
  
  We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (8)    (x1[2] ≥ 0∧[1] + [-1]x1[2] ≥ 0 ⇒ (U^Increasing(COND_2268_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)), ≥)∧[(-1)bni_14 + (-1)Bound*bni_14] + [(-1)bni_14]x1[2] ≥ 0∧[(-1)bso_15] ≥ 0)

  
  
  We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (9)    (x1[2] ≥ 0∧[1] + [-1]x1[2] ≥ 0 ⇒ (U^Increasing(COND_2268_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)), ≥)∧[(-1)bni_14 + (-1)Bound*bni_14] + [(-1)bni_14]x1[2] ≥ 0∧[(-1)bso_15] ≥ 0)

  
  
  We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (10)    (x1[2] ≥ 0∧[1] + [-1]x1[2] ≥ 0 ⇒ (U^Increasing(COND_2268_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)), ≥)∧[(-1)bni_14 + (-1)Bound*bni_14] + [(-1)bni_14]x1[2] ≥ 0∧[(-1)bso_15] ≥ 0)

  
  
  

To summarize, we get the following constraints P_≥ for the following pairs.

• COND_2268_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)
  
  • ((U^Increasing(2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)), ≥)∧[bni_12] = 0∧0 = 0∧[1 + (-1)bso_13] ≥ 0)
    
  
  
• 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3) → COND_2268_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)
  
  • (x1[2] ≥ 0∧[1] + [-1]x1[2] ≥ 0 ⇒ (U^Increasing(COND_2268_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)), ≥)∧[(-1)bni_14 + (-1)Bound*bni_14] + [(-1)bni_14]x1[2] ≥ 0∧[(-1)bso_15] ≥ 0)
    
  
  

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0   
POL(FALSE) = 0   
POL(COND_2268_0_INIT_GE1(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃   
POL(java.lang.Object(x₁)) = [-1]   
POL(Carre(x₁)) = [-1]   
POL(ARRAY(x₁)) = [-1]   
POL(3) = [3]   
POL(2268_0_INIT_GE(x₁, x₂, x₃)) = [-1] + [-1]x₂   
POL(+(x₁, x₂)) = x₁ + x₂   
POL(1) = [1]   
POL(0) = 0   
POL(&&(x₁, x₂)) = [-1]   
POL(>(x₁, x₂)) = [-1]   
POL(-1) = [-1]   
POL(<(x₁, x₂)) = [-1]   
POL(2) = [2]   

The following pairs are in P_>:

COND_2268_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)

The following pairs are in P_bound:

2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3) → COND_2268_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)

The following pairs are in P_≥:

2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3) → COND_2268_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)

There are no usable rules.

(36) Complex Obligation (AND)

(37) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
||	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(2): 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3) → COND_2268_0_INIT_GE1(x1[2] > -1 && x1[2] < 2, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)


The set Q is empty.

(38) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(39) TRUE

(40) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
||	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(3): COND_2268_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3) → 2268_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3] + 1, 0)


The set Q is empty.

(41) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(42) TRUE